GitOrigin-RevId: 33921f87ae3c1ca12ad8ba4a90a9a5bb2372d055

…les (#13254)

Run more tests with MOVE_COMPILER_V2=true, modifying drivers to put outputs in this case in .v2_exp files to allow slight variations from V1 outputs.  Filed separate issues for variations found.

GitOrigin-RevId: db482a4e89ae987e1ddc32d6698cf256803a9a40

GitOrigin-RevId: 4da21b944eb3300ab3466c0ff48b62c9c13fcff7

Fixes #12781

This also refactors and simplifies the releasing of references before write operations. I initially thought this was the problem but it wasn't, anyway the refactoring simplifies the code a bit.

GitOrigin-RevId: e93cd69e296c84b7f0fb11b025cc73ef91dd6bc1

* use  aptos production configs in one place and share them in the codebase

GitOrigin-RevId: 6582ad5efe9eb250b79c61473f89417881070b57

…resent (#13380)

Fix dependency path in a move-abigen test so it still works with a built
move-stdlib, while adding comments and
some Debug implementations to make it easier to sort out what paths
are present where in the code.

This PR also adds somewhat unnecessary dependences between stdlib
builds and tests using them, not because they use the built libs (they
should be reading the sources, not the built packages), but because
this leads to more deterministic output when paths are not specified
correctly.

GitOrigin-RevId: d57183418ba38281a144e62c1fe6752ef07e9727

GitOrigin-RevId: db53d9e0cd073d3377a552e2e2f7e1205e867cfa

* [extended checker] Add checks for safe randomness usage

This adds checks to the extended checker for safe usage of randomness.

- Public functions which directly or indirectly call into the `randomness` module are flagged as an error. Exempted functions are those which have the `#[lint_allow_unsafe_randomness]` attribute or which are in the framework at address 0x1.
- Private or friend entry functions which do not have the `#[randomness]` attribute are flagged as an error.

We do not need to check dynamic dispatch here since only public functions are allowed to be registered for dispatch, and those are already checked via above logic.

* Addressing reviewer comments, enabling `#[attribute_area::attribute_name]` syntax and using this for lint attributes.

GitOrigin-RevId: 92ba8946ae6ad4658d219a596b9fdccb0b514f5c

* fix address on scripts added by `run_spec_checker` so it is compatible with `is_script` function.
* update docgen test outputs with corrected contents

GitOrigin-RevId: ded3c0e921be176139d480e944796bf6366f6a46

…ecursively (#13442)

* fix recursive

* update v2 test

* refactor

GitOrigin-RevId: 11033f4dd27144908ad9832dd49dc86fe261561f

…ions (#13438)

* Graph output change

* [compiler-v2] Fixes bug in reference safety regards weak borrow relations

Fixes #12904

A weak borrow results from branching like `let r = if (cond) &mut r.f else &mut r.g`. The resulting reference `r` can be derived from either of the two borrows. The borrow safety check until now did not correctly deal with weak borrows when constructing hyper edges. This PR fixes the issue by grouping edges which target the same node into one hyper edge.

The 1st commit is only a change in annotation output, the 2nd is the relevant one for the change.

* Removing unnecessary complication in `group_children_into_hyper_edges`, addressing reviewer comments

GitOrigin-RevId: 15b5a55b1da3bf2e02119cfccb473457a3997422

This updates the `move_pr.sh` script to run the tests also covered by #13446 as integration tests, namely all kind of tests depending on the MOVE_COMPILER_V2 env var.

With `move_pr.sh -i2` both integration tests without the MOVE_COMPILER_V2 flag are run (the `-i` option) as with the flag set (`-2`). This mechanism was already before there, only the crate lists have been updated.

There are some `.v2_exp` files which did not exists or where out-of-date which are also updated with this PR.

We currently need a workaround to avoid `aptos-cached-packages` is build when MOVE_COMPILER_V2 is set, as this will generate new .md files for the framework based on some bug fixes the v2 compiler has, that appear as changes in the client. The script ensures that this crate is build before switching the env var to on.

As a sideffect, this also removes the 2nd dependency from RUST_BACKTRAC in exp files, in `move-compiler/src/diagnoses`. The same mechanism as already in place in `model.rs` is used: in order to get backtrace into error output, one must set both `RUST_BACKTRACE` and `MVC_BACKTRACE`.

GitOrigin-RevId: 7cb1e69c9432ad172eb052ab1fed94dac6a09c0f

Closes #13146

Adds a check that a global resource is not borrowed when it is declared in the access specifier list of a function.

This implements the full semantics of Move 2.0 access specifiers. However, if the 2.0 language is not enabled, access specifiers other then `acquires` will be rejected by the context checker, and for that special case the behavior is equivalent.

In order to test the extended access specifier semantics, we need to disable the existing acquires checker, which is not yet implemented for general access specifiers.

GitOrigin-RevId: 562cc9429de9625ed3d3ed551f0956946f4e6f9b

* [compiler-v2] Bytecode verification failure error message

This close #12709 and mitigates #12817.

If we had a bytecode verification failure post file format verification, until now we gave a cryptical error. We also have some weird corner cases where the verifier fails while reference safety is clearly maintained.

This improves the error message on bv failure, as well as prints out a special tailored message for the corner cases, which we will be hopefully able to fix with a new bytecode verifier. The full VMError detail
is omitted unless the env var MVC_BACKTRACE is set to true.

* Addressing reviewer comments

GitOrigin-RevId: 1d9cd70677a2fa76e993d5ad5a281d046dec6a19

* support mdx

* handle comments

GitOrigin-RevId: 6cad0ac954656bb7017e6c24e9b979f19c58024f

…13492)

* migrate tests including failed ones

* fix local transaction test discrepency issue

GitOrigin-RevId: 1fff3e89661968135ac5c8efe94794907080b9cf

- Entry function checks are simplified
- Function instantiations are created via dedicated APIs and so to execute a function loading has to be performed first.
- Script checks are nicer now inside loader
- LoadedFunctionInstantiation removed

GitOrigin-RevId: 71647131cf3632af86a2cd26a933fdcc10896ad5

- Created two DeFi examples, revamping the rounding error examples
  - One is a simple dex pool based on Uniswap V1
  - Another is a simple reserve-backed currency system
- Defined the safety properties for the examples, and proved them with Move Prover

GitOrigin-RevId: 9ec0c8d6e626350d3f86f1f41658785a36cdaeec

GitOrigin-RevId: 47606b9571880546b84c0d43c68b5e77b4a51002

Fixes #13625.

Fold all non-empty constant vectors, to avoid stack overflows in some cases.

GitOrigin-RevId: 4c0c0995a288e3605b4f7dabf53bdd25047ed872

This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time.

The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`.

The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605:

- Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug`
- Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>`
- Adds an option `--skip-instance-check` to completely turn off verification of type instantiations.
- Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long  and confusing when trying to understand what functions are verified

GitOrigin-RevId: 673023c706fe19d694b4f990e5a753e3ec24ad91

…d fields improvements (#15594)

GitOrigin-RevId: 2bea962eac4743db6cc0ae2e8a2fd7fcc323b121

…ove compile` and `aptos move lint` (#15540)

GitOrigin-RevId: f5d01316eea6f6475ac38c1343b2d0584ae8a162

Output using the `debug!` logging facility should not stay permanent in the code, or at leastr be protected by an additional guard, unless it is useful to work with end users. The default output of `debug!` should overall be useful for users to help understand their problems and avoid complex internal data structures.

This updates some code in the compiler to follow this guideline, as well as refines the docs for logging to reflect this.

This came apparent when trying to use `aptos move prove -v debug` -- the output printed lots of stuff which is probably only relevant for internal debugging.

GitOrigin-RevId: 6b09e6337deca18de4ec499bf02cfa0b44bdb461

…(#15627)

* tmp fix

* bugfix

* format

* fix bug and comment

---------

Co-authored-by: Zekun Wang <[email protected]>
GitOrigin-RevId: 20e25a4a2daf2e27a87030136da5d534da5dab8b

* fix bytecode deps for unit tests

* add tests

* linter & remove debug print

* reset Cargo.lock

* add bytecode files

* reset Cargo.lock

* add .gitkeep for empty dir

* address comments

* resolve merge conflicts

---------

Co-authored-by: Zekun Wang <[email protected]>
GitOrigin-RevId: aaa3514c8ee4e5d38b89d916eadff7286a42e040

GitOrigin-RevId: fc5f7f012b347f04b8c3f083bcaa47c44871475b

GitOrigin-RevId: 87767e8b1b831adffd7b36e1b652878756797ba5

GitOrigin-RevId: a1b900b8424df07696cd4832d0aa9c48ed8ce81d

GitOrigin-RevId: 8f877ab9e84002d88714b12ea71eb167fd141731

GitOrigin-RevId: 5514aee2374b69fe1d7c500930f3f3a35a76a8a3

GitOrigin-RevId: d00ae19a1c8617233897365da5f5ced570ff2fc3

Changes module caching logic for VM validator (mempool validation running prologues) to make it
work correctly with module publishing. When new modules are published and committed, the module
cache will detect the change and reload the new module.

GitOrigin-RevId: 745ec1d4db40f53c883f3d4d8e7960eb82baa956

Type tag cache can be kept even if tags are cached speculatively. Moving it
out to live together with struct name index map.

GitOrigin-RevId: e12fcbbd14d2c66a34ff778f02a5c68faab03a29

GitOrigin-RevId: 506903fe2d95880509f56582f05bfc3753e13a73

GitOrigin-RevId: 842bb853331553fce7595e3c4b02daadc5d5a4c9

* rc refcell for frame cache

* per instruction and cache tree - Bug chase

* found the bug

* progress

* added feature flag dispatch logic

* feature flag

* updated

* address review comments

* more comments addressed

* more review comments addressed

* fix wrong if logic

GitOrigin-RevId: 5334c850edb7d6af9851cd68bc8691b0bc63f34d

GitOrigin-RevId: e36868a5bc810699630facd7b066c76237184b1c

GitOrigin-RevId: 4b69e484b6abc1159407acaafbfaf7cdb349e26c

GitOrigin-RevId: d52887aba0e62bca345033dcefaba7de490f22d9

## Description
```
module aptos_framework::signing_data {
    enum SigningData has copy, drop {
        V1 { digest: vector<u8>, authenticator: vector<u8> },
    }

    #[test_only]
    public fun create_signing_data(digest: vector<u8>): SigningData {
        SigningData::V1 { digest }
    }

    public fun digest(signing_data: &SigningData): &vector<u8> {
        &signing_data.digest
    }

    public fun authenticator(signing_data: &SigningData): &vector<u8> {
        &signing_data.authenticator
    }
}
```
a function with the following signature can be used to authorize account..
```
/// The native function to dispatch customized move authentication function.
 native fun dispatchable_authenticate(
        account: signer,
        signing_data: SigningData,
        function: &FunctionInfo
    ): signer;
```

GitOrigin-RevId: 1d8460a995503574ec4e9699d3442d0150d7f3b9

…5739)

* Enhance fuzz.sh script with 'cmin' functionality for corpus minimization.
Introduce debug panic mechanism in errors.rs for improved error handling during fuzzing and update README.md for usage instructions.

* fmt

* rename
remove useless collect

GitOrigin-RevId: b2b3d67889a3550f238b1648144c5c25ef352bc0

Boogie is using exhaustive amounts of memory if run as part of proving aptos-framework (100GB+), which makes CI and local testing fail randomly. This PR introduces a new `--shards` option which splits the Boogie job into multiple shards, if specified. Also re-animates the use of `Prover.toml` in a package directory allowing to set such options.

GitOrigin-RevId: 4125bd8d78786ed26c916c8bf01707f3a3ec9714